package edu.lambdateacher.expressions;

/*
 LambdaTeacher
 Copyright (C) 2000  Kim Mason
 Copyright (C) 2014  Vitalij Zadneprovskij

 This program is free software; you can redistribute it and/or
 modify it under the terms of the GNU General Public License
 as published by the Free Software Foundation; either version 2
 of the License, or (at your option) any later version.

 This program is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU General Public License for more details.

 You should have received a copy of the GNU General Public License
 along with this program; if not, write to the Free Software
 Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
 */

import java.util.HashSet;
import java.util.Set;

import edu.lambdateacher.parser.LambdaTokenType;
import edu.lambdateacher.reductions.BetaReduction;

/**
 * The class Application represents a Lambda Application. It is a subclass of
 * Expression. Lambda Applications are of the form Expr1 Expr2, in which Expr1
 * can be thought of as a function, and Expr2 as an argument. Because of the
 * func-arg relationship, Applications are beta reducable (and therefore alpha
 * reducable as well).
 */
public class Application extends Expression implements Cloneable {
	private Expression func;
	private Expression arg;

	/**
	 * A simple constructor function, which sets everything to null.
	 */
	public Application() {
		super(); // this is implicit, but it can't hurt.
		setFunc(null);
		setArg(null);
	}

	/**
	 * A simple constructor which sets func and arg to the input parameters.
	 */
	public Application(Expression func, Expression arg) {
		super();
		this.setFunc(func);
		this.setArg(arg);
	}

	/**
	 * getFunc() simply returns the func of this Application (note it doesn't
	 * return a clone of the func).
	 */
	public final Expression getFunc() {
		return this.func;
	}

	// getFuncSkipBindings skips over any bindings to
	// get the body
	public final Expression getFuncSkipBindings() {
		Expression tempexpr;

		tempexpr = this.getFunc();
		while (tempexpr instanceof Binding) {
			tempexpr = ((Binding) tempexpr).getExpr();
		}
		return tempexpr;
	}

	/**
	 * setFunc simply sets the function of this Application the the parameter
	 * (not a clone of the parameter).
	 */
	public final void setFunc(Expression infunc) {
		this.func = infunc;
		if (infunc != null){
			if (infunc.getParentModified()){
				this.setParentModified(true);
			}
		}
	}

	public final Expression getArg() {
		return this.arg;
	}

	// getArgSkipBindings skips over any bindings to
	// get the body
	public final Expression getArgSkipBindings() {
		Expression tempexpr;

		tempexpr = this.getArg();
		while (tempexpr instanceof Binding) {
			tempexpr = ((Binding) tempexpr).getExpr();
		}
		return tempexpr;
	}

	public final void setArg(Expression inarg) {
		this.arg = inarg;
		if (inarg != null){
			if (inarg.getParentModified()){
				this.setParentModified(true);
			}
		}
	}

	/**
	 * Override the clone method in superclass Object. Simply clones the func
	 * and arg, then creates a new Application with the new func and arg.
	 */
	public Object clone() {
		Application toreturn = (Application) super.clone();
		Expression thefunc = null;
		Expression thearg = null;

		if (this.getFunc() != null){
			thefunc = (Expression) this.getFunc().clone();
		}
		if (this.getArg() != null){
			thearg = (Expression) this.getArg().clone();
		}
		toreturn.setFunc(thefunc);
		toreturn.setArg(thearg);
		return toreturn;
	}

	/**
	 * containsUnbound returns true if this Application contains the instring as
	 * an unbound variable within func or arg.
	 */
	public boolean containsUnbound(String inname) {
		if (inname == null)
			return false;

		boolean infunc = false;
		boolean inarg = false;

		if (this.getFunc() != null) {
			infunc = this.getFunc().containsUnbound(inname);
		}
		if (this.getArg() != null) {
			inarg = this.getArg().containsUnbound(inname);
		}

		return (infunc | inarg);
	}

	/**
	 * beta_allowed returns true if beta reduction is allowed. This means that
	 * the func must be an Abstraction (after skipping bindings), and must have
	 * a valid bound variable. An alternative is the func is a numerical
	 * operator or a half applied numerical operator, and the arg is a number.
	 * The arg shouldn't be null.
	 */
	public boolean betaAllowed() {
		// keep skipping bindings until the function part is reached
		Expression thefunc = getFuncSkipBindings();
		Expression thearg = getArgSkipBindings();
		
		return BetaReduction.betaAllowed(thefunc, thearg, this.getArg());
	}

	/**
	 * beta_reduce subs arg into the body of function, and returns the new body
	 * if beta_allowed. It also sets parentmodified to true, because beta
	 * reducing should wipe out all upper bindings.
	 */
	public Expression betaReduce() {
		return BetaReduction.betaReduce(this);
	}

	/**
	 * unParse simply returns a string containing this Application unparsed. if
	 * verbose then use lots of brackets.
	 */
	public String stringRepresentation(boolean verbose) {
		String thestring = "";
		Expression thefunc = this.getFunc();

		if (verbose == false){
			thestring = thestring + "(";
		}

		if (thefunc != null) {
			if (verbose) {
				thestring = thestring + "(" + thefunc.stringRepresentation(verbose) + ")";
			} else {
				thestring = thestring + thefunc.stringRepresentation(verbose);
			}
		}
		Expression thearg = this.getArg();

		if (thearg != null){
			if (verbose) {
				thestring = thestring + "(" + thearg.stringRepresentation(verbose) + ")";
			} else {
				thestring = thestring + thearg.stringRepresentation(verbose);
			}
		}

		if (verbose == false){
			thestring = thestring + ")";
		}
		return thestring;
	}

	/**
	 * 
	 * nameSubstitute simply replaces any variables with name matching inname
	 * with a clone of param.
	 * @param inname regular expression to be matched
	 * @param param expression to replace the matching params 
	 * @return nameSubstitute returns the new expression with
	 * the necessary variables replaced. If either of the parentmodifieds in the
	 * subbed func or arg are true, the parentmodified of the returned
	 * expression is set to true. This is because name subs destroy upper
	 * bindings.
	 */
	public Expression nameSubstitute(String inname, Expression param) {
		// we can't sub into a name that doesn't exist.
		if (inname == null){
			return this;
		}

		Application toreturn = null;
		Expression newfunc = null;
		Expression newarg = null;

		Expression oldfunc = getFunc();
		Expression oldarg = getArg();

		if (oldfunc != null) {
			newfunc = oldfunc.nameSubstitute(inname, param);
		}

		if (oldarg != null) {
			newarg = oldarg.nameSubstitute(inname, param);
		}

		toreturn = this;
		this.setFunc(newfunc);
		this.setArg(newarg);

		return toreturn;
	}

	/**
	 * containsReducable returns true if this Application can be beta reduced,
	 * or any of the sub Expressions are reducable.
	 */
	public boolean containsReducable() {
		boolean funcreducable = false;
		boolean argreducable = false;

		if (this.betaAllowed() == true){
			return true;
		}

		if (this.getFunc() != null) {
			funcreducable = this.getFunc().containsReducable();
		}
		if (this.getArg() != null) {
			argreducable = this.getArg().containsReducable();
		}
		return funcreducable | argreducable;
	}

	/**
	 * normal_reduce attempts to beta reduce the current Application. If this
	 * can't be done, it attempts to normal reduce the func, and if this can't
	 * be done, it attempts to reduce the arg. It then returns the reduced
	 * expressions, with everything cloned whether it was modified or not.
	 */
	public Expression normalReduce() {
		// first attempt to beta reduce the current Application
		if (betaAllowed()) {
			Expression toreturn = this.betaReduce();
			return toreturn;
		}

		Expression oldfunc = this.getFunc();
		Expression oldarg = this.getArg();
		Expression newfunc = null;
		Expression newarg = null;

		// determine whether we can reduce the func
		boolean funccontainsreducable = false;
		if (oldfunc != null){
			funccontainsreducable = oldfunc.containsReducable();
		}

		if (funccontainsreducable) {
			newfunc = oldfunc.normalReduce();
			if (oldarg != null){
				newarg = oldarg;
			}

			Application toreturn = this;
			this.setFunc(newfunc);
			this.setArg(newarg);

			return toreturn;
		}

		// if we made it to here, we haven't reduced the func,
		// so determine whether the arg is reducable
		boolean argcontainsreducable = false;
		if (oldarg != null){
			argcontainsreducable = oldarg.containsReducable();
		}

		if (argcontainsreducable) {
			if (oldfunc != null){
				newfunc = oldfunc;
			}
				
			newarg = oldarg.normalReduce();

			Application toreturn = this;
			this.setFunc(newfunc);
			this.setArg(newarg);

			return toreturn;
		}

		// if we made it to here, neither the func or arg are reducable,
		// so return the current Application.
		return this;
	}

	/*
	 * reduceExpression simply searches for inexpr, and if the current
	 * expression is equal to inexpr, it reduces it and returns the result.
	 */
	public Expression reduceExpression(Expression inexpr) {
		// if this is the expression to reduce, try to reduce it.
		if (this == inexpr) {

			Expression toreturn = this.betaReduce();
			return toreturn;
		}

		// attempt to reduce in the function and arg
		Expression oldfunc = this.getFunc();
		Expression oldarg = this.getArg();
		Expression newfunc = null;
		Expression newarg = null;

		if (oldfunc != null) {
			newfunc = oldfunc.reduceExpression(inexpr);
		}

		if (oldarg != null) {
			newarg = oldarg.reduceExpression(inexpr);
		}

		Application toreturn = this;
		toreturn.setFunc(newfunc);
		toreturn.setArg(newarg);

		return toreturn;
	}

	/**
	 * If this Application is beta reducable, this is returned, otherwise the
	 * func is tried, otherwise the arg.
	 */
	public Expression findNormalReducable() {
		// is the current Application Reducable?
		if (betaAllowed()) {
			return this;
		}

		Expression oldfunc = this.getFunc();
		Expression oldarg = this.getArg();

		// determine whether we can reduce the func
		boolean funccontainsreducable = false;
		if (oldfunc != null){
			funccontainsreducable = oldfunc.containsReducable();
		}

		if (funccontainsreducable) {
			return oldfunc.findNormalReducable();
		}

		// if we made it to here, the func wasn't reducable
		// so determine whether the arg is reducable
		boolean argcontainsreducable = false;
		if (oldarg != null){
			argcontainsreducable = oldarg.containsReducable();
		}
			
		if (argcontainsreducable) {
			return oldarg.findNormalReducable();
		}

		// if we made it to here, neither the func or arg are reducable,
		// so return null
		return null;
	}

	/**
	 * findApplicativeReducable attempts to find the applicative reducable
	 * subexpression of the current Expression
	 */
	public Expression findApplicativeReducable() {
		// first check for applicative reducable in the func
		Expression tempfunc = this.getFunc();
		Expression toreturn = null;
		if (tempfunc != null){
			toreturn = tempfunc.findApplicativeReducable();
		}

		if (toreturn != null){
			return toreturn;
		}

		// then check for applicative reducable in the arg
		Expression temparg = this.getArg();
		if (temparg != null){
			toreturn = temparg.findApplicativeReducable();
		}
			
		if (toreturn != null){
			return toreturn;
		}

		// is the current Application Reducable?
		if (betaAllowed()) {
			return this;
		}

		return toreturn;
	}

	/**
	 * findUnboundVars returns a HashSet with the names of all of the unbound
	 * variables in the current expression. The input HashSet (bound_vars)
	 * contains all of the variable names that are bound.
	 */
	public Set findUnboundVars(Set bound_vars) {
		Set funcset = new HashSet();
		Set argset = new HashSet();

		if (this.getFunc() != null){
			funcset = this.getFunc().findUnboundVars(bound_vars);
		}

		if (this.getArg() != null){
			funcset = this.getArg().findUnboundVars(bound_vars);
		}

		HashSet<LambdaTokenType> toreturn = new HashSet<LambdaTokenType>(funcset);
		toreturn.addAll(argset);

		return toreturn;
	}

	/*
	 * removeAllBindings walks down the expression tree, and removes any
	 * bindings that it finds.
	 */
	public Expression removeAllBindings() {
		Expression oldfunc = this.getFunc();
		Expression oldarg = this.getArg();

		if (oldfunc != null) {
			Expression newfunc = oldfunc.removeAllBindings();
			this.setFunc(newfunc);
		}
		if (oldarg != null) {
			Expression newarg = oldarg.removeAllBindings();
			this.setArg(newarg);
		}
		return this;
	}

	/*
	 * removeBinding walks down the expression tree, and removes any occurences
	 * of the input parameter (toremove).
	 */
	public Expression removeBinding(Binding toremove) {
		Expression oldfunc = this.getFunc();
		Expression oldarg = this.getArg();

		if (oldfunc != null) {
			Expression newfunc = oldfunc.removeBinding(toremove);
			this.setFunc(newfunc);
		}
		if (oldarg != null) {
			Expression newarg = oldarg.removeBinding(toremove);
			this.setArg(newarg);
		}
		return this;
	}
}
